Move vector initialization 2 loops out, to reduce the number of
re-alloactions.

When using an index to point into the learnts vector, make sure the items
in that vector are valid, or in release mode are dropped to not crash the
solver. This was found when using LCM which modified the learnts vector.

The tmp dir variable has been read from $3, while $2 was the actual aim.

In the old version, the wrong variable has been used as index value,
leading to out of bound errors.

If there are no candidate literals to compute a score for, stop the
computation, and skip.

The split variable next has to be initialized, such that in case of
failures during computing the candidates, e.g. due to too small formulas,
there lit_Undef value can still be returned.

Consequently, make sure nobody consumes lit_Undef as an index.

As getting stuck might be due to a race condition, allow the solver to
see this condition more often before actually aborting the search. On the
other hand, make sure we assert before exit, so that debugging would be
doable, and the problem can be identified during fuzzing.

When multiple slaves work on the same node, make sure they do not overwrite
the state of each other. Only set a state to unknown, if the node actually
has an unknown state.

Currently, the stopUnsatChilds option had to be set to write the unsat
state for a node. However, the state should always be written. Hence, the
check for the option is moved closer to actually running the related
algorithm.

In the reduceDB, new clauses are added to the clauses to be shared, but
no clauses are removed. This way, faulty pointers might be used, as the
clauses that are shared might become invalid, or wrong indexes are used.

When we know a level does not have clauses to share, do not lock the level,
but instead skip the level right away.